(*************************************************************************)
(** Simply-typed Scalina  in Coq.    Regularity                          *)
(** Author: Adriaan Moors, 2008                                          *)
(*************************************************************************)

(** Based on the Coq tutorial at POPL 2008, see
    "Engineering Formal Metatheory", Aydemir, Charguéraud, Pierce,
    Pollack, Weirich. POPL 2008.

    Tutorial authors: Brian Aydemir and Stephanie Weirich, with help
    from Aaron Bohannon, Nate Foster, Benjamin Pierce, Jeffrey
    Vaughan, Dimitrios Vytiniotis, and Steve Zdancewic.  Adapted from
    code by Arthur Charguéraud.
*)

Set Implicit Arguments.
Require Import Metatheory Scalina_Definitions Scalina_Induction Scalina_SubstFresh Scalina_Env support.
Require Import List.


Lemma lc_tp_implies_lc_mems_rt_expand: forall (T: tp) (ms: list mem),
  lc_tp T -> rt_expand T ms -> (forall t: tm, lc_tm t -> lc_mems (open_mems ms t)).
Proof.
  intros T ms Hlc Hexp.
  induction Hexp.
  induction o; inversion Hlc. subst. intros.
  pick_fresh x. forward~ (H2 x). intros. fold (open_mems ms x) in H0. 
  assert (x \notin fv_mems ms) as FrMs by auto.
  apply (@lc_open_mems x t ms H FrMs H0).

  pick_fresh x. forward~ (H0 x). intros. fold (open_mems ms x) in H0. 
  assert (x \notin fv_mems ms) as FrMs by auto.
  apply (@lc_open_mems x t ms H2 FrMs H1).
Qed.


Lemma member_lookup_preserves_lc: forall (o: option tp) (mems : list mem) (l : lab) (T : tp) t,
 lc_tp (tp_struct o mems) -> option_has T (mems ?: l) -> lc_tm t  -> lc_tp ({0 ~tp> t}T).
Proof. 
  intros.

  functional induction (mems_lookup l mems); simpl in H0.
    contradiction.
    subst T. functional induction (mem_getLabel m'). 
     induction o. inversion H. pick_fresh y. forward~ (H4 y). intros Hlcms. inversion Hlcms.
     inversion H7. simpl in *. 
 
     apply (@lc_open_tp y _ _x0 H1); auto*. 

     simpl in *. apply (@lc_open_tp y _ _x0 H1); auto*. 
     simpl in *. inversion H. pick_fresh x. forward~ (H2 x). intros Hlcms. inversion Hlcms. 
       inversion H5; apply (@lc_open_tp x _ _x0 H1); auto*. 

     apply IHo0; auto*. 
       inversion H.
       pick_fresh x.  forward~ (H3 x). intros Hlcms. inversion Hlcms. fold (open_mems E' x) in *.
       assert (x \notin fv_mems E') as FrE by auto*.
       apply lc_struct_noself with (L:= L).
       intros x0 Fr0. fold (open_mems E' x0). 
       eapply lc_open_mems; eauto.

       pick_fresh x. forward~ (H5 x). intros Hlcms. inversions Hlcms. fold (open_mems E' x) in *.
       assert (x \notin fv_mems E') as FrE by auto*.
       apply lc_struct_self with (L:= L); trivial. 
       intros x0 Fr0. fold (open_mems E' x0). 
       eapply lc_open_mems; eauto.
Qed.

Lemma typing_regular : 
 (forall (E : env) (t : tm) (T : tp) (t1 : E |= t ~: T), wf_env E /\ lc_tm t /\ lc_tp T) /\ (*lc_tp T is needed for lc_mem case*)
 (forall (E : env) (T : tp) (w : E |= T ~::Struct), wf_env E /\ lc_tp T) /\
 (forall (E : env) (T : tp) (w : E |= T ~::Concrete), wf_env E /\ lc_tp T) /\
 (forall (E : env) (T : tp) (R: tp) (w : E |= T ~< R), wf_env E /\ lc_tp T /\ lc_tp R) /\
 (forall (E : env) (w : wf_env E), wf_env E) /\
 (forall (E : env) (m : mem) (w : E |= m ~:::wf), wf_env E /\ lc_mem m) /\
 (forall (E : env) (ms : list mem) (w : E |= ms ~:::wfs), wf_env E /\ lc_mems ms).
Proof.
  apply typing_wf_mutual_ind; intros; first[progress auto*| splits; destructs H; auto*].

  apply member_lookup_preserves_lc with (o := o) (mems := mems) (l := l); auto*.

  apply_fresh lc_struct_self as x; auto*. 
    fold (open_mems ms x). pick_fresh x'. forward~ (H x'). intros Hlcms. destructs Hlcms.
    assert (x' \notin fv_mems ms) as FrE by auto*.
    eapply lc_open_mems; eauto.

  apply_fresh lc_struct_noself as x; auto*. inversion H1. 
    fold (open_mems ms x). pick_fresh x'. forward~ (H4 x'). intros Hlcms. destructs Hlcms.
    assert (x' \notin fv_mems ms) as FrE by auto*.
    eapply lc_open_mems; eauto.
Qed.    


(** morale: option_has in lc_mem leads to stupid induction principle *)

Lemma value_regular : forall e,
  value e -> lc_tm e.
Proof.
  induction 1; auto*.
Qed.

(*
Lemma rt_lookup_agrees_forAll: forall (f: mem -> Prop) ms l m,
  list_forAll (map f ms) -> f mems_lookup_mem l ms.
Proof.
  intros f ms l m Hall Hlu.
  induction Hlu; simpl in *; auto*.
Qed.*)



Lemma red_regular : forall e e',
  red e e' -> lc_tm e /\ lc_tm e'.
Proof.
  induction 1. inversion H. inversion H3. split. auto*. 

  pose (l0:= lc_tp_implies_lc_mems_rt_expand H5 H0).
  unfold open_mems in l0. pose (l1:= lc_mems_forAll (l0 (new T) H3)). rewrite map_map in l1. clear l0. 

  clear H0. (*otherwise induction hypothesis becomes too strong*)
  functional induction (mems_lookup l ms).   
    contradiction.
    (* case: found member with right label *)
    clear e0. 
    simpl in H1. functional induction (mem_getRhs m').
    unfold mem_getLabel in *. (*don't perform functional induction, it breaks the proof!*)
    induction o. 
      simpl in H1. subst. simpl in l1. destruct l1 as [Hlcmem _]. inversion Hlcmem. auto*.
      contradiction.

    (*inductive case *)
    simpl in l1. destruct l1 as [_ ForTail]. apply (IHo H1 ForTail).
  
  auto*.
Qed.

(*
*** Local Variables: ***
*** coq-prog-args: ("-emacs-U"  "-I" "../lib" "-I" "../metatheory") ***
*** End: ***
*)